\begin{nusmvCommand}{compute} {Performs computation of quantitative characteristics}

\cmdLine{compute [-h] [-m | -o output-file] [-n number | -p \linebreak"compute-expr [IN context]"]}

This command deals with the computation of quantitative
characteristics of real time systems. It is able to compute the length
of the shortest (longest) path from two given set of states.
\begin{center}
\code{MAX [ alpha , beta ]} \\
\code{MIN [ alpha , beta ]} 
\end{center}
Properties of the above form can be specified in the input file via
the keyword \code{COMPUTE} or directly at command line, using option
\commandopt{p}.

If there exists an infinite path beginning in a state in
\textit{start} that never reaches a state in \textit{final}, then
\textit{infinity} is returned. If any of the initial or final states 
is empty, then \textit{undefined} is returned.

Option \commandopt{n} can be used for computing a particular
expression in the model. If neither \commandopt{n} nor \commandopt{p}
are used, all the COMPUTE specifications are computed.

It is important to remark here that if the FSM is not total (i.e. it
contains deadlock states) \reserved{COMPUTE} may produce wrong
results. It is possible to check the FSM against deadlock states by
calling the command \command{check\_fsm}.

\begin{cmdOpt}

\opt{-m}{Pipes the output generated by the command in processing
\code{COMPUTE}{s} to the program specified by the \shellvar{PAGER} shell
variable if defined, else through the \unix command
\shellcommand{more}.}

\opt{-o \parameter{\filename{output-file}}}{Writes the output generated by the command in
processing \code{COMPUTE}{s} to the file \filename{output-file}.}

\opt{-p \parameter{"\compexpr [IN context]"}}{A COMPUTE formula to be checked.
\code{context} is the module instance name which the variables in
\compexpr must be evaluated in.}

\opt{-n \parameter{\natnum{number}}}{Computes only the property with index \natnum{number}.}

\end{cmdOpt}
\end{nusmvCommand}
